package lattice.traveler;

import lattice.Computation;

public class LatticeTraveler {

	/**
	 * Returns the CGS that satisfies the predicate of the specified computation.
	 * The whole distributed lattice is traversed using the lexical traversing
	 * algorithm proposed by Dr. Vijay Garg in "Enumerating Global States of a
	 * Distributed Computation."
	 * 
	 * @param c the specified computation
	 * @return null if no such CGS exists
	 */
	public static SyncedStateCut lexTraverse(Computation c) {
		int n = c.objNum();		// number of shared object
		SyncedStateCut G = new SyncedStateCut();
		int[] K = new int[n];	// succ(G, k)
		int[] H = new int[n];	// leastConsistent(K)
		SyncedStateCut m = new SyncedStateCut();
		
		for (int i = 0; i < n; ++i) { 
			G.addVid(0); // initial current CGS to the very beginning of the computation
			m.addVid(c.stateNum(i)-1); // size of the list of events = number of events at Pi
		}
		
		while (!G.greater(m)) {
			if (c.evaluate(G)) return G;
			if (G.equals(m)) return null;
			
			// decide k
			int k = n-1;
			for (; k >= 0; --k) {
				if (G.getVid(k) != m.getVid(k)) { // if next event on Pk exists
					VectorClock e = c.getClock(k, G.getVid(k)+1); // next event on Pk after G[k]
					boolean enabled = true;
					for (int j = 0; j < n; ++j) {
						if (j != k && e.get(j) > G.getVid(j)) enabled = false;
					}
					if (enabled) break;
				}
			}
			
			// compute K := succ(G, k)
			for (int i = 0; i < k; ++i) K[i] = G.getVid(i);
			K[k] = G.getVid(k) + 1;
			for (int i = k+1; i < n; ++i) K[i] = 0;
			
			// compute H := leastConsistent(K)
			for (int i = 0; i < n; ++i) H[i] = K[i];
			for (int i = 0; i < n; ++i) {
				for (int j = 0; j < n; ++j) {
					H[j] = Math.max(H[j], (c.getClock(i, K[i])).get(j));
				}
			}
			
			// G := H
			for (int i = 0; i < n; ++i) G.setVid(i, H[i]);
		}
		
		return null;
	}
}
